@i locl(a) occurs once
== e@i.es-kind(es; e) = locl(a)
==  alle-at(es;
==  alle-at(i;
==  alle-at(e.alle-at(es;
==  alle-at(e.alle-at(i;
==  alle-at(e.alle-at(e'.((es-kind(es; e) = locl(a))  (es-kind(es; e') = locl(a))  (e = e')))
==  alle-at() 

latex

---

clarification:

once-p(es;i;a)
== existse-at(es; i; e.(es-kind(es; e) = locl(a)  Knd))
==  alle-at(es;
==  alle-at(i;
==  alle-at(e.alle-at(es;
==  alle-at(e.alle-at(i;
==  alle-at(e.alle-at(e'.((es-kind(es; e) = locl(a)  Knd)
==  alle-at(e.alle-at( (es-kind(es; e') = locl(a)  Knd)
==  alle-at(e.alle-at( (e = e'  es-E(es))))) 

latex

Definitions	P  Q, e@i.P(e), alle-at(es; i; e.P(e)), P  Q, Knd, es-kind(es; e), locl(a), s = t, es-E(es)
FDL editor aliases	once-p